Termination proof of /tmp/tmpFsSaJm/PALINDROME

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isPalListKind: empty set
U13: {1}
isNeList: empty set
U21: {1}
U22: {1}
U23: {1}
U24: {1}
U25: {1}
isList: empty set
U26: {1}
U31: {1}
U32: {1}
U33: {1}
isQid: empty set
U41: {1}
U42: {1}
U43: {1}
U44: {1}
U45: {1}
U46: {1}
U51: {1}
U52: {1}
U53: {1}
U54: {1}
U55: {1}
U56: {1}
U61: {1}
U62: {1}
U63: {1}
U71: {1}
U72: {1}
U73: {1}
isPal: empty set
U74: {1}
U81: {1}
U82: {1}
U83: {1}
isNePal: empty set
U91: {1}
U92: {1}
a: empty set
e: empty set
i: empty set
o: empty set
u: empty set

↳ CSR

  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

The replacement map contains the following entries:

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92, __¹, U13¹, U26¹, U33¹, U46¹, U56¹, U63¹, U74¹, U83¹, U92¹} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U12¹, U11¹, U22¹, U21¹, U23¹, U24¹, U25¹, U32¹, U31¹, U42¹, U41¹, U43¹, U44¹, U45¹, U52¹, U51¹, U53¹, U54¹, U55¹, U62¹, U61¹, U72¹, U71¹, U73¹, U82¹, U81¹, U91¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPALLISTKIND, ISNELIST, ISLIST, ISQID, ISPAL, ISNEPAL} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)
U11¹(tt, V) → U12¹(isPalListKind(V), V)
U11¹(tt, V) → ISPALLISTKIND(V)
U12¹(tt, V) → U13¹(isNeList(V))
U12¹(tt, V) → ISNELIST(V)
U21¹(tt, V1, V2) → U22¹(isPalListKind(V1), V1, V2)
U21¹(tt, V1, V2) → ISPALLISTKIND(V1)
U22¹(tt, V1, V2) → U23¹(isPalListKind(V2), V1, V2)
U22¹(tt, V1, V2) → ISPALLISTKIND(V2)
U23¹(tt, V1, V2) → U24¹(isPalListKind(V2), V1, V2)
U23¹(tt, V1, V2) → ISPALLISTKIND(V2)
U24¹(tt, V1, V2) → U25¹(isList(V1), V2)
U24¹(tt, V1, V2) → ISLIST(V1)
U25¹(tt, V2) → U26¹(isList(V2))
U25¹(tt, V2) → ISLIST(V2)
U31¹(tt, V) → U32¹(isPalListKind(V), V)
U31¹(tt, V) → ISPALLISTKIND(V)
U32¹(tt, V) → U33¹(isQid(V))
U32¹(tt, V) → ISQID(V)
U41¹(tt, V1, V2) → U42¹(isPalListKind(V1), V1, V2)
U41¹(tt, V1, V2) → ISPALLISTKIND(V1)
U42¹(tt, V1, V2) → U43¹(isPalListKind(V2), V1, V2)
U42¹(tt, V1, V2) → ISPALLISTKIND(V2)
U43¹(tt, V1, V2) → U44¹(isPalListKind(V2), V1, V2)
U43¹(tt, V1, V2) → ISPALLISTKIND(V2)
U44¹(tt, V1, V2) → U45¹(isList(V1), V2)
U44¹(tt, V1, V2) → ISLIST(V1)
U45¹(tt, V2) → U46¹(isNeList(V2))
U45¹(tt, V2) → ISNELIST(V2)
U51¹(tt, V1, V2) → U52¹(isPalListKind(V1), V1, V2)
U51¹(tt, V1, V2) → ISPALLISTKIND(V1)
U52¹(tt, V1, V2) → U53¹(isPalListKind(V2), V1, V2)
U52¹(tt, V1, V2) → ISPALLISTKIND(V2)
U53¹(tt, V1, V2) → U54¹(isPalListKind(V2), V1, V2)
U53¹(tt, V1, V2) → ISPALLISTKIND(V2)
U54¹(tt, V1, V2) → U55¹(isNeList(V1), V2)
U54¹(tt, V1, V2) → ISNELIST(V1)
U55¹(tt, V2) → U56¹(isList(V2))
U55¹(tt, V2) → ISLIST(V2)
U61¹(tt, V) → U62¹(isPalListKind(V), V)
U61¹(tt, V) → ISPALLISTKIND(V)
U62¹(tt, V) → U63¹(isQid(V))
U62¹(tt, V) → ISQID(V)
U71¹(tt, I, P) → U72¹(isPalListKind(I), P)
U71¹(tt, I, P) → ISPALLISTKIND(I)
U72¹(tt, P) → U73¹(isPal(P), P)
U72¹(tt, P) → ISPAL(P)
U73¹(tt, P) → U74¹(isPalListKind(P))
U73¹(tt, P) → ISPALLISTKIND(P)
U81¹(tt, V) → U82¹(isPalListKind(V), V)
U81¹(tt, V) → ISPALLISTKIND(V)
U82¹(tt, V) → U83¹(isNePal(V))
U82¹(tt, V) → ISNEPAL(V)
U91¹(tt, V2) → U92¹(isPalListKind(V2))
U91¹(tt, V2) → ISPALLISTKIND(V2)
ISLIST(V) → U11¹(isPalListKind(V), V)
ISLIST(V) → ISPALLISTKIND(V)
ISLIST(__(V1, V2)) → U21¹(isPalListKind(V1), V1, V2)
ISLIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(V) → U31¹(isPalListKind(V), V)
ISNELIST(V) → ISPALLISTKIND(V)
ISNELIST(__(V1, V2)) → U41¹(isPalListKind(V1), V1, V2)
ISNELIST(__(V1, V2)) → ISPALLISTKIND(V1)
ISNELIST(__(V1, V2)) → U51¹(isPalListKind(V1), V1, V2)
ISNEPAL(V) → U61¹(isPalListKind(V), V)
ISNEPAL(V) → ISPALLISTKIND(V)
ISNEPAL(__(I, __(P, I))) → U71¹(isQid(I), I, P)
ISNEPAL(__(I, __(P, I))) → ISQID(I)
ISPAL(V) → U81¹(isPalListKind(V), V)
ISPAL(V) → ISPALLISTKIND(V)
ISPALLISTKIND(__(V1, V2)) → U91¹(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 4 SCCs with 38 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPSubtermProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U91¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPALLISTKIND} are not replacing on any position.

The TRS P consists of the following rules:

U91¹(tt, V2) → ISPALLISTKIND(V2)
ISPALLISTKIND(__(V1, V2)) → U91¹(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ISPALLISTKIND(__(V1, V2)) → U91¹(isPalListKind(V1), V2)
ISPALLISTKIND(__(V1, V2)) → ISPALLISTKIND(V1)

The remaining pairs can at least be oriented weakly.

U91¹(tt, V2) → ISPALLISTKIND(V2)

Used ordering: Combined order from the following AFS and order.
ISPALLISTKIND(x1) = x1
U91¹(x1, x2) = x2

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

U91¹(tt, V2) → ISPALLISTKIND(V2)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U71¹, U72¹, U81¹, U82¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISNEPAL, ISPAL} are not replacing on any position.

The TRS P consists of the following rules:

ISNEPAL(__(I, __(P, I))) → U71¹(isQid(I), I, P)
U71¹(tt, I, P) → U72¹(isPalListKind(I), P)
U72¹(tt, P) → ISPAL(P)
ISPAL(V) → U81¹(isPalListKind(V), V)
U81¹(tt, V) → U82¹(isPalListKind(V), V)
U82¹(tt, V) → ISNEPAL(V)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ISNEPAL(__(I, __(P, I))) → U71¹(isQid(I), I, P)

The remaining pairs can at least be oriented weakly.

U71¹(tt, I, P) → U72¹(isPalListKind(I), P)
U72¹(tt, P) → ISPAL(P)
ISPAL(V) → U81¹(isPalListKind(V), V)
U81¹(tt, V) → U82¹(isPalListKind(V), V)
U82¹(tt, V) → ISNEPAL(V)

Used ordering: Combined order from the following AFS and order.
U71¹(x1, x2, x3) = x3
ISNEPAL(x1) = x1
U72¹(x1, x2) = x2
ISPAL(x1) = x1
U81¹(x1, x2) = x2
U82¹(x1, x2) = x2

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ QCSDependencyGraphProof

          ↳ QCSDP

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U72¹, U71¹, U81¹, U82¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISPAL, ISNEPAL} are not replacing on any position.

The TRS P consists of the following rules:

U71¹(tt, I, P) → U72¹(isPalListKind(I), P)
U72¹(tt, P) → ISPAL(P)
ISPAL(V) → U81¹(isPalListKind(V), V)
U81¹(tt, V) → U82¹(isPalListKind(V), V)
U82¹(tt, V) → ISNEPAL(V)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 5 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91, U12¹, U41¹, U42¹, U43¹, U44¹, U45¹, U51¹, U52¹, U53¹, U54¹, U55¹, U11¹, U21¹, U22¹, U23¹, U24¹, U25¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U12¹(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U41¹(isPalListKind(V1), V1, V2)
U41¹(tt, V1, V2) → U42¹(isPalListKind(V1), V1, V2)
U42¹(tt, V1, V2) → U43¹(isPalListKind(V2), V1, V2)
U43¹(tt, V1, V2) → U44¹(isPalListKind(V2), V1, V2)
U44¹(tt, V1, V2) → U45¹(isList(V1), V2)
U45¹(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → U51¹(isPalListKind(V1), V1, V2)
U51¹(tt, V1, V2) → U52¹(isPalListKind(V1), V1, V2)
U52¹(tt, V1, V2) → U53¹(isPalListKind(V2), V1, V2)
U53¹(tt, V1, V2) → U54¹(isPalListKind(V2), V1, V2)
U54¹(tt, V1, V2) → U55¹(isNeList(V1), V2)
U55¹(tt, V2) → ISLIST(V2)
ISLIST(V) → U11¹(isPalListKind(V), V)
U11¹(tt, V) → U12¹(isPalListKind(V), V)
ISLIST(__(V1, V2)) → U21¹(isPalListKind(V1), V1, V2)
U21¹(tt, V1, V2) → U22¹(isPalListKind(V1), V1, V2)
U22¹(tt, V1, V2) → U23¹(isPalListKind(V2), V1, V2)
U23¹(tt, V1, V2) → U24¹(isPalListKind(V2), V1, V2)
U24¹(tt, V1, V2) → U25¹(isList(V1), V2)
U25¹(tt, V2) → ISLIST(V2)
U24¹(tt, V1, V2) → ISLIST(V1)
U54¹(tt, V1, V2) → ISNELIST(V1)
U44¹(tt, V1, V2) → ISLIST(V1)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The following rules are not useable and can be deleted:

__(__(x0, x1), x2) → __(x0, __(x1, x2))
__(x0, nil) → x0
__(nil, x0) → x0
U61(tt, x0) → U62(isPalListKind(x0), x0)
U62(tt, x0) → U63(isQid(x0))
U63(tt) → tt
U71(tt, x0, x1) → U72(isPalListKind(x0), x1)
U72(tt, x0) → U73(isPal(x0), x0)
U73(tt, x0) → U74(isPalListKind(x0))
U74(tt) → tt
U81(tt, x0) → U82(isPalListKind(x0), x0)
U82(tt, x0) → U83(isNePal(x0))
U83(tt) → tt
isNePal(x0) → U61(isPalListKind(x0), x0)
isNePal(__(x0, __(x1, x0))) → U71(isQid(x0), x0, x1)
isPal(x0) → U81(isPalListKind(x0), x0)
isPal(nil) → tt

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U92, U13, U33, U26, U46, U56} are replacing on all positions.
For all symbols f in {U91, U11, U12, U31, U32, U41, U42, U43, U44, U45, U21, U22, U23, U24, U25, U51, U52, U53, U54, U55, U12¹, U41¹, U42¹, U43¹, U44¹, U45¹, U51¹, U52¹, U53¹, U54¹, U55¹, U11¹, U21¹, U22¹, U23¹, U24¹, U25¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isList, isNeList, isQid, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U12¹(tt, V) → ISNELIST(V)
ISNELIST(__(V1, V2)) → U41¹(isPalListKind(V1), V1, V2)
U41¹(tt, V1, V2) → U42¹(isPalListKind(V1), V1, V2)
U42¹(tt, V1, V2) → U43¹(isPalListKind(V2), V1, V2)
U43¹(tt, V1, V2) → U44¹(isPalListKind(V2), V1, V2)
U44¹(tt, V1, V2) → U45¹(isList(V1), V2)
U45¹(tt, V2) → ISNELIST(V2)
ISNELIST(__(V1, V2)) → U51¹(isPalListKind(V1), V1, V2)
U51¹(tt, V1, V2) → U52¹(isPalListKind(V1), V1, V2)
U52¹(tt, V1, V2) → U53¹(isPalListKind(V2), V1, V2)
U53¹(tt, V1, V2) → U54¹(isPalListKind(V2), V1, V2)
U54¹(tt, V1, V2) → U55¹(isNeList(V1), V2)
U55¹(tt, V2) → ISLIST(V2)
ISLIST(V) → U11¹(isPalListKind(V), V)
U11¹(tt, V) → U12¹(isPalListKind(V), V)
ISLIST(__(V1, V2)) → U21¹(isPalListKind(V1), V1, V2)
U21¹(tt, V1, V2) → U22¹(isPalListKind(V1), V1, V2)
U22¹(tt, V1, V2) → U23¹(isPalListKind(V2), V1, V2)
U23¹(tt, V1, V2) → U24¹(isPalListKind(V2), V1, V2)
U24¹(tt, V1, V2) → U25¹(isList(V1), V2)
U25¹(tt, V2) → ISLIST(V2)
U24¹(tt, V1, V2) → ISLIST(V1)
U54¹(tt, V1, V2) → ISNELIST(V1)
U44¹(tt, V1, V2) → ISLIST(V1)

The TRS R consists of the following rules:

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
isNeList(V) → U31(isPalListKind(V), V)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U33(tt) → tt
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U46(tt) → tt
U13(tt) → tt

Q is empty.

Using the order
Polynomial interpretation [25]:

POL(ISLIST(x₁)) = 2·x₁
POL(ISNELIST(x₁)) = 2·x₁
POL(U11(x₁, x₂)) = 2·x₁
POL(U11¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U12(x₁, x₂)) = 2·x₁
POL(U12¹(x₁, x₂)) = 2·x₁ + 2·x₂
POL(U13(x₁)) = 0
POL(U21(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + 2·x₃
POL(U21¹(x₁, x₂, x₃)) = 1 + x₁ + 2·x₂ + 2·x₃
POL(U22(x₁, x₂, x₃)) = x₂ + 2·x₃
POL(U22¹(x₁, x₂, x₃)) = 1 + x₁ + 2·x₂ + 2·x₃
POL(U23(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(U23¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U24(x₁, x₂, x₃)) = 2·x₁ + x₃
POL(U24¹(x₁, x₂, x₃)) = x₁ + 2·x₂ + 2·x₃
POL(U25(x₁, x₂)) = 0
POL(U25¹(x₁, x₂)) = x₁ + 2·x₂
POL(U26(x₁)) = 0
POL(U31(x₁, x₂)) = 2
POL(U32(x₁, x₂)) = 1 + 2·x₁
POL(U33(x₁)) = 1
POL(U41(x₁, x₂, x₃)) = 2 + 2·x₁
POL(U41¹(x₁, x₂, x₃)) = 2 + 2·x₂ + 2·x₃
POL(U42(x₁, x₂, x₃)) = 0
POL(U42¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U43(x₁, x₂, x₃)) = 2·x₁
POL(U43¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U44(x₁, x₂, x₃)) = x₁
POL(U44¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U45(x₁, x₂)) = 0
POL(U45¹(x₁, x₂)) = 2·x₂
POL(U46(x₁)) = 0
POL(U51(x₁, x₂, x₃)) = 2 + x₁
POL(U51¹(x₁, x₂, x₃)) = 2 + 2·x₂ + 2·x₃
POL(U52(x₁, x₂, x₃)) = 1
POL(U52¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U53(x₁, x₂, x₃)) = 1
POL(U53¹(x₁, x₂, x₃)) = 1 + 2·x₂ + 2·x₃
POL(U54(x₁, x₂, x₃)) = x₁
POL(U54¹(x₁, x₂, x₃)) = 2·x₂ + 2·x₃
POL(U55(x₁, x₂)) = 0
POL(U55¹(x₁, x₂)) = 2·x₂
POL(U56(x₁)) = 0
POL(U91(x₁, x₂)) = 2·x₁
POL(U92(x₁)) = 2·x₁
POL(__(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(a) = 2
POL(e) = 2
POL(i) = 1
POL(isList(x₁)) = 2·x₁
POL(isNeList(x₁)) = 2
POL(isPalListKind(x₁)) = 0
POL(isQid(x₁)) = 2·x₁
POL(nil) = 0
POL(o) = 0
POL(tt) = 0
POL(u) = 0

the following usable rules

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt

could all be oriented weakly.
Since all dependency pairs and these rules are strongly conservative, this is sound.
Furthermore, the pairs

ISNELIST(__(V1, V2)) → U41¹(isPalListKind(V1), V1, V2)
U41¹(tt, V1, V2) → U42¹(isPalListKind(V1), V1, V2)
U44¹(tt, V1, V2) → U45¹(isList(V1), V2)
ISNELIST(__(V1, V2)) → U51¹(isPalListKind(V1), V1, V2)
U51¹(tt, V1, V2) → U52¹(isPalListKind(V1), V1, V2)
U53¹(tt, V1, V2) → U54¹(isPalListKind(V2), V1, V2)
ISLIST(__(V1, V2)) → U21¹(isPalListKind(V1), V1, V2)
U23¹(tt, V1, V2) → U24¹(isPalListKind(V2), V1, V2)
U44¹(tt, V1, V2) → ISLIST(V1)

could be oriented strictly and thus removed.
The pairs

U12¹(tt, V) → ISNELIST(V)
U42¹(tt, V1, V2) → U43¹(isPalListKind(V2), V1, V2)
U43¹(tt, V1, V2) → U44¹(isPalListKind(V2), V1, V2)
U45¹(tt, V2) → ISNELIST(V2)
U52¹(tt, V1, V2) → U53¹(isPalListKind(V2), V1, V2)
U54¹(tt, V1, V2) → U55¹(isNeList(V1), V2)
U55¹(tt, V2) → ISLIST(V2)
ISLIST(V) → U11¹(isPalListKind(V), V)
U11¹(tt, V) → U12¹(isPalListKind(V), V)
U21¹(tt, V1, V2) → U22¹(isPalListKind(V1), V1, V2)
U22¹(tt, V1, V2) → U23¹(isPalListKind(V2), V1, V2)
U24¹(tt, V1, V2) → U25¹(isList(V1), V2)
U25¹(tt, V2) → ISLIST(V2)
U24¹(tt, V1, V2) → ISLIST(V1)
U54¹(tt, V1, V2) → ISNELIST(V1)

could only be oriented weakly and must be analyzed further.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSUsableRulesProof

              ↳ QCSDP

                ↳ QCSDPReductionPairProof

                  ↳ QCSDP

                    ↳ QCSDependencyGraphProof

          ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U92, U13, U33, U26, U46, U56} are replacing on all positions.
For all symbols f in {U91, U11, U12, U31, U32, U41, U42, U43, U44, U45, U21, U22, U23, U24, U25, U51, U52, U53, U54, U55, U12¹, U43¹, U42¹, U44¹, U45¹, U53¹, U52¹, U55¹, U54¹, U11¹, U22¹, U21¹, U23¹, U25¹, U24¹} we have µ(f) = {1}.
The symbols in {isPalListKind, isList, isNeList, isQid, ISNELIST, ISLIST} are not replacing on any position.

The TRS P consists of the following rules:

U12¹(tt, V) → ISNELIST(V)
U42¹(tt, V1, V2) → U43¹(isPalListKind(V2), V1, V2)
U43¹(tt, V1, V2) → U44¹(isPalListKind(V2), V1, V2)
U45¹(tt, V2) → ISNELIST(V2)
U52¹(tt, V1, V2) → U53¹(isPalListKind(V2), V1, V2)
U54¹(tt, V1, V2) → U55¹(isNeList(V1), V2)
U55¹(tt, V2) → ISLIST(V2)
ISLIST(V) → U11¹(isPalListKind(V), V)
U11¹(tt, V) → U12¹(isPalListKind(V), V)
U21¹(tt, V1, V2) → U22¹(isPalListKind(V1), V1, V2)
U22¹(tt, V1, V2) → U23¹(isPalListKind(V2), V1, V2)
U24¹(tt, V1, V2) → U25¹(isList(V1), V2)
U25¹(tt, V2) → ISLIST(V2)
U24¹(tt, V1, V2) → ISLIST(V1)
U54¹(tt, V1, V2) → ISNELIST(V1)

The TRS R consists of the following rules:

isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
isNeList(V) → U31(isPalListKind(V), V)
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt
U33(tt) → tt
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U45(tt, V2) → U46(isNeList(V2))
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U46(tt) → tt
U13(tt) → tt

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs with 12 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92, __¹} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal} are not replacing on any position.

The TRS P consists of the following rules:

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

__¹(__(X, Y), Z) → __¹(X, __(Y, Z))
__¹(__(X, Y), Z) → __¹(Y, Z)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
__¹(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ AND

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

          ↳ QCSDP

            ↳ QCSDPSubtermProof

              ↳ QCSDP

                ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U13, U26, U33, U46, U56, U63, U74, U83, U92} are replacing on all positions.
For all symbols f in {U11, U12, U21, U22, U23, U24, U25, U31, U32, U41, U42, U43, U44, U45, U51, U52, U53, U54, U55, U61, U62, U71, U72, U73, U81, U82, U91} we have µ(f) = {1}.
The symbols in {isPalListKind, isNeList, isList, isQid, isPal, isNePal} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt, V) → U12(isPalListKind(V), V)
U12(tt, V) → U13(isNeList(V))
U13(tt) → tt
U21(tt, V1, V2) → U22(isPalListKind(V1), V1, V2)
U22(tt, V1, V2) → U23(isPalListKind(V2), V1, V2)
U23(tt, V1, V2) → U24(isPalListKind(V2), V1, V2)
U24(tt, V1, V2) → U25(isList(V1), V2)
U25(tt, V2) → U26(isList(V2))
U26(tt) → tt
U31(tt, V) → U32(isPalListKind(V), V)
U32(tt, V) → U33(isQid(V))
U33(tt) → tt
U41(tt, V1, V2) → U42(isPalListKind(V1), V1, V2)
U42(tt, V1, V2) → U43(isPalListKind(V2), V1, V2)
U43(tt, V1, V2) → U44(isPalListKind(V2), V1, V2)
U44(tt, V1, V2) → U45(isList(V1), V2)
U45(tt, V2) → U46(isNeList(V2))
U46(tt) → tt
U51(tt, V1, V2) → U52(isPalListKind(V1), V1, V2)
U52(tt, V1, V2) → U53(isPalListKind(V2), V1, V2)
U53(tt, V1, V2) → U54(isPalListKind(V2), V1, V2)
U54(tt, V1, V2) → U55(isNeList(V1), V2)
U55(tt, V2) → U56(isList(V2))
U56(tt) → tt
U61(tt, V) → U62(isPalListKind(V), V)
U62(tt, V) → U63(isQid(V))
U63(tt) → tt
U71(tt, I, P) → U72(isPalListKind(I), P)
U72(tt, P) → U73(isPal(P), P)
U73(tt, P) → U74(isPalListKind(P))
U74(tt) → tt
U81(tt, V) → U82(isPalListKind(V), V)
U82(tt, V) → U83(isNePal(V))
U83(tt) → tt
U91(tt, V2) → U92(isPalListKind(V2))
U92(tt) → tt
isList(V) → U11(isPalListKind(V), V)
isList(nil) → tt
isList(__(V1, V2)) → U21(isPalListKind(V1), V1, V2)
isNeList(V) → U31(isPalListKind(V), V)
isNeList(__(V1, V2)) → U41(isPalListKind(V1), V1, V2)
isNeList(__(V1, V2)) → U51(isPalListKind(V1), V1, V2)
isNePal(V) → U61(isPalListKind(V), V)
isNePal(__(I, __(P, I))) → U71(isQid(I), I, P)
isPal(V) → U81(isPalListKind(V), V)
isPal(nil) → tt
isPalListKind(a) → tt
isPalListKind(e) → tt
isPalListKind(i) → tt
isPalListKind(nil) → tt
isPalListKind(o) → tt
isPalListKind(u) → tt
isPalListKind(__(V1, V2)) → U91(isPalListKind(V1), V2)
isQid(a) → tt
isQid(e) → tt
isQid(i) → tt
isQid(o) → tt
isQid(u) → tt

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.